diff options
| author | Enrico Tassi | 2021-03-18 19:15:39 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-03-26 15:19:19 +0100 |
| commit | 34ece1ae3e6696bdc9556e5019c3b8ec3fd23f8a (patch) | |
| tree | f304cf0ce7c7b89dc008cf1e36b1ef00891b19c8 /tactics | |
| parent | c2ed2e395f2164ebbc550e70899c49af23e1ad1e (diff) | |
[recordops] complete API rewrite; the module is now called [structures]
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 5e9c3baeb1..31b276bb3e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -320,7 +320,7 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (cst,_) -> - (match Recordops.find_primitive_projection cst with + (match Structures.PrimitiveProjections.find_opt cst with | Some p -> let p = Projection.make p false in let npars = Projection.npars p in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67bf8d0d29..decf19588f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1555,7 +1555,7 @@ let make_projection env sigma params cstr sign elim i n c u = | Some proj -> let args = Context.Rel.to_extended_vect mkRel 0 sign in let proj = - match Recordops.find_primitive_projection proj with + match Structures.PrimitiveProjections.find_opt proj with | Some proj -> mkProj (Projection.make proj false, mkApp (c, args)) | None -> @@ -1585,7 +1585,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let params = List.map EConstr.of_constr params in let cstr = (get_constructors env indf).(0) in let elim = - try DefinedRecord (Recordops.lookup_projections ind) + try DefinedRecord (Structures.Structure.find_projections ind) with Not_found -> let u = EInstance.kind sigma u in let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in |