diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/contradiction.ml | 4 | ||||
| -rw-r--r-- | tactics/eqdecide.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 |
3 files changed, 7 insertions, 7 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 768d6860dc..fe44559ed8 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -20,7 +20,7 @@ module NamedDecl = Context.Named.Declaration (* Absurd *) let mk_absurd_proof t = - let build_coq_not () = EConstr.of_constr (build_coq_not ()) in + let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in let id = Namegen.default_dependent_ident in mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]), mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) @@ -35,7 +35,7 @@ let absurd c = let t = j.Environ.utj_val in let tac = Tacticals.New.tclTHENLIST [ - elim_type (EConstr.of_constr (build_coq_False ())); + elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())); Simple.apply (mk_absurd_proof t) ] in Sigma.Unsafe.of_pair (tac, sigma) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 641929a77b..bda25d7f02 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -106,8 +106,8 @@ let solveNoteqBranch side = let make_eq () = (*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let build_coq_not () = EConstr.of_constr (build_coq_not ()) -let build_coq_sumbool () = EConstr.of_constr (build_coq_sumbool ()) +let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) +let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ()) let mkDecideEqGoal eqonleft op rectype c1 c2 = let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in diff --git a/tactics/equality.ml b/tactics/equality.ml index f9f9b9dd7c..0a68ff1291 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -934,9 +934,9 @@ let build_selector env sigma dirn c ind special default = let ci = make_case_info env ind RegularStyle in mkCase (ci, p, c, Array.of_list brl) -let build_coq_False () = EConstr.of_constr (build_coq_False ()) -let build_coq_True () = EConstr.of_constr (build_coq_True ()) -let build_coq_I () = EConstr.of_constr (build_coq_I ()) +let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()) +let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ()) +let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ()) let rec build_discriminator env sigma dirn c = function | [] -> |