From 95dd7304f68eb155f572bf221c4d99fca85b700c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 23 Mar 2008 22:11:25 +0000
Subject: Fix a bug found by B. Grégoire when declaring morphisms in module
 types. Change (again) the semantics of bindings and the binding modifier ! in
 typeclasses. Inside [ ], implicit binding where only parameters need to be
 given is the default, use ! to use explicit binding, which is equivalent to
 regular bindings except for generalization of free variables. Outside
 brackets (e.g. on the right of instance declarations),  explicit binding is
 the default, and implicit binding can be used by adding ! in front. This
 avoids almost every use of ! in the standard library and in other examples I
 have.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 31 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 16 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a3baa1abb7..4f740f8652 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -973,11 +973,11 @@ END
     
 let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
 
-let declare_instance a aeq n s = ((dummy_loc,Name n),Explicit,
-				  CApp (dummy_loc, (None, mkRefC (Qualid (dummy_loc, qualid_of_string s))), 
-					[(a,None);(aeq,None)]))
+let declare_instance a aeq n s = ((dummy_loc,Name n), Explicit,
+				 CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), 
+					  [a;aeq]))
 
-let anew_instance instance fields = new_instance [] instance fields None (fun _ -> ())
+let anew_instance instance fields = new_instance [] instance fields None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1104,6 +1104,7 @@ let declare_projection n instance_id r =
   let c = constr_of_global r in
   let term = respect_projection c ty in
   let typ = Typing.type_of (Global.env ()) Evd.empty term in
+  let ctx, typ = Sign.decompose_prod_assum typ in
   let typ =
     let n = 
       let rec aux t = 
@@ -1122,6 +1123,7 @@ let declare_projection n instance_id r =
     let ctx,ccl = Reductionops.decomp_n_prod (Global.env()) Evd.empty (3 * n) typ
     in it_mkProd_or_LetIn ccl ctx 
   in
+  let typ = it_mkProd_or_LetIn typ ctx in
   let cst = 
     { const_entry_body = term;
       const_entry_type = Some typ;
@@ -1209,18 +1211,15 @@ VERNAC COMMAND EXTEND AddSetoid1
       [ init_setoid ();
 	let instance_id = add_suffix n "_Morphism" in
 	let instance = 
-	  ((dummy_loc,Name instance_id), Implicit,
-	  CApp (dummy_loc, (None, mkRefC 
-	    (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism"))), 
-	       [(s,None);(m,None)]))
-	in
-	  if Lib.is_modtype () then (context ~hook:(fun r -> declare_projection n instance_id r) [ instance ])
-	  else (
-	    Flags.silently 
-	      (fun () ->
-		ignore(new_instance [] instance [] None (fun cst -> declare_projection n instance_id (ConstRef cst)));
-		Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
-	    Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ())
+	  ((dummy_loc,Name instance_id), Explicit,
+	  CAppExpl (dummy_loc, 
+		   (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), 
+		   [cHole; s; m]))
+	in	  
+	let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
+	  ignore(new_instance [] instance []
+		    ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
+		    None)
       ]
 END
 
-- 
cgit v1.2.3