diff options
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 10 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 48 |
2 files changed, 26 insertions, 32 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 8c4dc0e8a6..b94b1fc657 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,8 +1,6 @@ -let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook - ~opaque ~poly ~udecl ~types:tyopt ~body sigma - let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.(IsDefinition Definition) ~opaque:false ~impargs:[] ~udecl sigma body None + let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kind = Decls.(IsDefinition Definition) in + DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl + ~opaque:false ~poly ~types:None ~body sigma diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 820063c25c..35e131020b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1864,14 +1864,14 @@ let proper_projection env sigma r ty = Array.append args [| instarg |]) in it_mkLambda_or_LetIn app ctx -let declare_projection n instance_id r = +let declare_projection name instance_id r = let poly = Global.is_polymorphic r in let env = Global.env () in let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in let ty = Retyping.get_type_of env sigma c in - let term = proper_projection env sigma c ty in - let sigma, typ = Typing.type_of env sigma term in + let body = proper_projection env sigma c ty in + let sigma, typ = Typing.type_of env sigma body in let ctx, typ = decompose_prod_assum sigma typ in let typ = let n = @@ -1892,14 +1892,11 @@ let declare_projection n instance_id r = let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ in it_mkProd_or_LetIn ccl ctx in - let typ = it_mkProd_or_LetIn typ ctx in - let univs = Evd.univ_entry ~poly sigma in - let typ = EConstr.to_constr sigma typ in - let term = EConstr.to_constr sigma term in - let cst = Declare.definition_entry ~types:typ ~univs term in - let _ : Constant.t = - Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition) - (Declare.DefinitionEntry cst) + let types = Some (it_mkProd_or_LetIn typ ctx) in + let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let impargs, udecl = [], UState.default_univ_decl in + let _r : GlobRef.t = + DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma in () let build_morphism_signature env sigma m = @@ -1927,10 +1924,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.minimize_universes evd in - let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in - Pretyping.check_evars env evd (EConstr.of_constr m); - Evd.evar_universe_context evd, m + evd, morph let default_morphism sign m = let env = Global.env () in @@ -1965,22 +1959,24 @@ let add_morphism_as_parameter atts m n : unit = let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in - let uctx, instance = build_morphism_signature env evd m in - let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in - let cst = Declare.declare_constant ~name:instance_id - ~kind:Decls.(IsAssumption Logical) - (Declare.ParameterEntry (None,(instance,uctx),None)) - in - Classes.add_instance (Classes.mk_instance - (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (GlobRef.ConstRef cst)); - declare_projection n instance_id (GlobRef.ConstRef cst) + let poly = atts.polymorphic in + let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let impargs, udecl = [], UState.default_univ_decl in + let evd, types = build_morphism_signature env evd m in + let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in + let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in + let cst = GlobRef.ConstRef cst in + Classes.add_instance + (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst); + declare_projection n instance_id cst let add_morphism_interactive atts m n : Lemmas.t = init_setoid (); let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in - let uctx, instance = build_morphism_signature env evd m in + let evd, morph = build_morphism_signature env evd m in let poly = atts.polymorphic in let kind = Decls.(IsDefinition Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in @@ -1996,7 +1992,7 @@ let add_morphism_interactive atts m n : Lemmas.t = let info = Lemmas.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in + let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in fst (Lemmas.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = |