diff options
| author | Maxime Dénès | 2017-05-28 22:40:55 +0200 |
|---|---|---|
| committer | GitHub | 2017-05-28 22:40:55 +0200 |
| commit | c05bfbee9a753b8867bc6ea5847cb7dd696a0cbd (patch) | |
| tree | 05b01f9c1103fde7486e4ae770139f3da58526ec /mathcomp | |
| parent | 20d1012d25093970ea72b928794cfdde27757e50 (diff) | |
| parent | 039aa8b0e6c5eb9fd0622494efa57acfaae7749e (diff) | |
Merge pull request #126 from ejgallego/coqlib-part-02
[coqlib] Update to explicitly build terms from references.
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index ce2456b..f98a251 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -3519,7 +3519,7 @@ let genclrtac cl cs clr = (apply_type cl cs) (fun type_err gl -> tclTHEN - (tclTHEN (Proofview.V82.of_tactic (elim_type (EConstr.of_constr (build_coq_False ())))) (cleartac clr)) + (tclTHEN (Proofview.V82.of_tactic (elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())))) (cleartac clr)) (fun gl -> raise type_err) gl)) (cleartac clr) @@ -5032,7 +5032,7 @@ let lz_setoid_relation = | env', srel when env' == env -> srel | _ -> let srel = - try Some (coq_constant "Class_setoid" sdir "RewriteRelation") + try Some (Universes.constr_of_global @@ coq_reference "Class_setoid" sdir "RewriteRelation") with _ -> None in last_srel := (env, srel); srel @@ -5078,7 +5078,7 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (EConstr.of_constr pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (build_coq_True ())) then + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ())) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else |