diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 4 | ||||
| -rw-r--r-- | vernac/metasyntax.mli | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 27 |
3 files changed, 8 insertions, 25 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 1bb9e0da19..3be3575985 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -606,8 +606,8 @@ let distribute a ll = List.map (fun l -> a @ l) ll t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *) let expand_list_rule typ tkl x n p ll = - let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in + let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in + let main = GramConstrNonTerminal (ETConstr typ, camlp5_message_name) in let tks = List.map (fun x -> GramConstrTerminal x) tkl in let rec aux i hds ll = if i < p then aux (i+1) (main :: tks @ hds) ll diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index b3049f1b7a..e064b570e6 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -51,7 +51,7 @@ val add_syntax_extension : val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit -(** Print the Camlp4 state of a grammar *) +(** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t diff --git a/vernac/record.ml b/vernac/record.ml index d9af5378f4..16b95a5ef4 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -369,26 +369,10 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) -let structure_signature ctx = - let rec deps_to_evar evm l = - match l with [] -> Evd.empty - | [decl] -> - let env = Environ.empty_named_context_val in - let (evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in - evm - | decl::tl -> - let env = Environ.empty_named_context_val in - let (evm, ev) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in - let new_tl = Util.List.map_i - (fun pos decl -> - RelDecl.map_type (fun t -> EConstr.Unsafe.to_constr (Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t))) decl) 1 tl in - deps_to_evar evm new_tl in - deps_to_evar Evd.empty (List.rev ctx) - open Typeclasses let declare_structure finite ubinders univs id idbuild paramimpls params arity template - fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = + fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers = let nparams = List.length params and nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in @@ -444,7 +428,7 @@ let implicits_of_context ctx = 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class finite def cum ubinders univs id idbuild paramimpls params arity - template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = + template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) let len = List.length params in @@ -500,7 +484,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari in let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields - ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign + ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) in let coers = List.map2 (fun coe pri -> Option.map (fun b -> @@ -607,12 +591,11 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in - let sign = structure_signature (fields@params) in let gr = match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild - implpars params arity template implfs fields is_coe coers priorities sign in + implpars params arity template implfs fields is_coe coers priorities in gr | _ -> let implfs = List.map @@ -631,7 +614,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf in let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs - fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in + fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in IndRef ind in Declare.declare_univ_binders gr pl; |