diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:01:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:21:25 +0100 |
| commit | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch) | |
| tree | 45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /plugins/micromega | |
| parent | cca57bcd89770e76e1bcc21eb41756dca2c51425 (diff) | |
| parent | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff) | |
Merge branch 'master'.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 82218a35c..5b56fb35b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1535,26 +1535,26 @@ let rec apply_ids t ids = | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids let coq_Node = - EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") + lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")) let coq_Leaf = - EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") + lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")) let coq_Empty = - EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") + lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")) let coq_VarMap = - EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") + lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")) let rec dump_varmap typ m = match m with - | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |]) - | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|]) - | Mc.Node(l,o,r) -> - Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) + | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |]) + | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|]) + | Mc.Node(l,o,r) -> + Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) let vm_of_list env = @@ -1727,7 +1727,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); + ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl)) |