Commit 90f26183 authored by charguer's avatar charguer

fix generator letval

parent 3a649d5c
Set Implicit Arguments.
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************)
(*
let test_poly () = let x = [] in x
*)
Lemma test_poly_spec : forall A,
Spec test_poly () |B>>
B \[] (fun (x:list A) => \[x = @nil A]).
Proof.
intros. xcf.
apply local_erase. intros x Ex.
xret.
hsimpl.
subst x. auto.
Qed.
Set Implicit Arguments.
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************)
......
......@@ -370,10 +370,10 @@ let rec coq_of_imp_cf cf =
| Cf_letval (x, fvs_strict, fvs_other, typ, v, cf) ->
let type_of_x = coq_forall_types fvs_strict typ in
let equ = coq_eq (Coq_var x) v in
let equ = coq_eq (Coq_var x) (coq_fun_types fvs_strict v) in
let conc = coq_apps (coq_of_cf cf) [h;q] in
funhq "tag_let_val" (*~label:x*) (Coq_forall ((x, type_of_x), Coq_impl (equ, conc)))
(*(!!L x: (fun H Q => forall (x:forall Ai,T), x = v -> F H Q)) *)
(*(!!L x: (fun H Q => forall (x:forall Ai,T), x = (fun Ai => v) -> F H Q)) *)
| Cf_letfunc (ncs, cf) ->
let ns, cs = List.split ncs in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment