diff options
| author | Enrico Tassi | 2019-05-24 14:57:33 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:43 +0200 |
| commit | a7a6fa3219134004f1fc6c757f1c16281724f38f (patch) | |
| tree | 3d0653067a9ea3c574b6237f6f8d0c5adae72450 /plugins | |
| parent | d77604cb06fcc8e8f38ef979627aa7a7138ef0f2 (diff) | |
[vernac] more precise types for Add Morph, Instance, and Function
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 12 |
2 files changed, 8 insertions, 8 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index bb6db1f5cf..241da053b7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in None, evd,List.rev rev_pconstants | _ -> - let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in + ComFixpoint.do_fixpoint Global false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -448,7 +448,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - pstate,evd,List.rev rev_pconstants + None,evd,List.rev rev_pconstants let generate_correction_proof_wf f_ref tcc_lemma_ref diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c568f63903..caeedadbf4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1796,11 +1796,11 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance atts binders (name,t) fields = let program_mode = atts.program in - let _id, proof = Classes.new_instance ~program_mode atts.polymorphic - name binders t (Some (true, CAst.make @@ CRecord (fields))) + let _id = Classes.new_instance ~program_mode atts.polymorphic + name binders t (true, CAst.make @@ CRecord (fields)) ~global:atts.global ~generalize:false Hints.empty_hint_info in - assert (Option.is_empty proof) (* refine:false with term *) + () let declare_instance_refl atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" @@ -2024,12 +2024,12 @@ let add_morphism atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = Classes.new_instance + let _id, pstate = Classes.new_instance_interactive ~program_mode:atts.program ~global:atts.global atts.polymorphic - instance_name binders instance_t None + instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - Option.get pstate (* no instance body -> always open proof *) + pstate (* no instance body -> always open proof *) (** Bind to "rewrite" too *) |