diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /plugins/cc/cctac.ml | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 150319f6b9..7dec34d4d7 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -13,6 +13,7 @@ open Names open Inductiveops open Declarations open Term +open Constr open EConstr open Vars open Tactics @@ -76,11 +77,11 @@ let rec decompose_term env sigma t= let (mind,i_ind),u = c in let u = EInstance.kind sigma u in let canon_mind = MutInd.make1 (MutInd.canonical mind) in - let canon_ind = canon_mind,i_ind in (Symb (Term.mkIndU (canon_ind,u))) + let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) | Const (c,u) -> let u = EInstance.kind sigma u in let canon_const = Constant.make1 (Constant.canonical c) in - (Symb (Term.mkConstU (canon_const,u))) + (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> let canon_const kn = Constant.make1 (Constant.canonical kn) in let p' = Projection.map canon_const p in @@ -198,7 +199,7 @@ let make_prb gls depth additionnal_terms = (fun decl -> let id = NamedDecl.get_id decl in begin - let cid=Term.mkVar id in + let cid=Constr.mkVar id in match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b |