- Correct handling of DependentMorphism error, using tclFAIL instead of

  letting the exception go uncatched.
- Reorder definitions in Morphisms, move the PER on (R ==> R') in
  Morphisms where it can be declared properly. Add an instance for
  Equivalence => Per.
- Change bug#1604 test file to the new semantics of [setoid_rewrite at]
- More unicode characters parsed by coqdoc.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 154 insertions, 112 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index afefeabb3..bbeeb4e03 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -512,6 +512,8 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
+exception DependentMorphism
+
 let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t option) (f : 'a -> constr) =
   let new_evar isevars env t =
     Evarutil.e_new_evar isevars env
@@ -528,8 +530,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
     let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in
       match kind_of_term t, l with
       | Prod (na, ty, b), obj :: cstrs -> 
-	  if dependent (mkRel 1) ty then 
-	    raise (Invalid_argument "build_signature: cannot handle dependent morphisms");
+	  if dependent (mkRel 1) ty then raise DependentMorphism;
 	  let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
 	  let ty = Reductionops.nf_betaiota ty in
 	  let relty = mk_relty ty obj in
@@ -842,21 +843,34 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
 			  decomp_pointwise nargs rel, mkApp(c1, args), mkApp(c2, args))
 			in Some res, occ
 		else rewrite_args occ
-		  
-	  | Prod (_, x, b) when not (dependent (mkRel 1) b) -> 
-	      let x', occ = aux env x occ None in
-	      let b = subst1 mkProp b in
-	      let b', occ = aux env b occ None in
-	      let res = 
-		if x' = None && b' = None then None
-		else 
-		  Some (resolve_morphism env sigma t
-			   ~fnewt:unfold_impl
-			   (arrow_morphism (Typing.type_of env sigma x) (Typing.type_of env sigma b))
-			   [| x ; b |] [| x' ; b' |]
-			   cstr evars)
-	      in res, occ
 		
+	  | Prod (n, x, b) when not (dependent (mkRel 1) b) -> 
+	      let x', occ = aux env x occ None in
+(* 		if x' = None && flags.under_lambdas then *)
+(* 		  let lam = mkLambda (n, x, b) in *)
+(* 		  let lam', occ = aux env lam occ None in *)
+(* 		  let res =  *)
+(* 		    match lam' with *)
+(* 		    | None -> None *)
+(* 		    | Some (prf, (car, rel, c1, c2)) -> *)
+(* 			Some (resolve_morphism env sigma t *)
+(* 				 ~fnewt:unfold_all *)
+(* 				 (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *)
+(* 				 cstr evars) *)
+(* 		  in res, occ *)
+(* 		else *)
+		  let b = subst1 mkProp b in
+		  let b', occ = aux env b occ None in
+		  let res = 
+		    if x' = None && b' = None then None
+		    else 
+		      Some (resolve_morphism env sigma t
+			       ~fnewt:unfold_impl
+			       (arrow_morphism (Typing.type_of env sigma x) (Typing.type_of env sigma b))
+			       [| x ; b |] [| x' ; b' |]
+			       cstr evars)
+		  in res, occ
+		    
 	  | Prod (n, ty, b) ->
 	      let lam = mkLambda (n, ty, b) in
 	      let lam', occ = aux env lam occ None in
@@ -910,60 +924,65 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
   let evars = ref (Evd.create_evar_defs Evd.empty) in
   let env = pf_env gl in
   let sigma = project gl in
-  let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars in
+  let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars 
+  in
     match eq with  
-	Some (p, (_, _, oldt, newt)) -> 
-	  (try 
-	      evars := Typeclasses.resolve_typeclasses env ~fail:true !evars;
-	      let p = Evarutil.nf_isevar !evars p in
-	      let newt = Evarutil.nf_isevar !evars newt in
-	      let undef = Evd.undefined_evars !evars in
-	      let abs = Option.map (fun (x, y) -> Evarutil.nf_isevar !evars x,
-		Evarutil.nf_isevar !evars y) !hypinfo.abs in
-	      let rewtac = 
-		match is_hyp with
-		  | Some id -> 
-		      let term = 
-			match abs with
-			    None -> p
-			  | Some (t, ty) -> 
-			      mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
-		      in
-			cut_replacing id newt 
-			  (fun x -> Tactics.refine (mkApp (term, [| mkVar id |])))
-		  | None -> 
-		      (match abs with
-			  None -> 
-			    let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
-			      tclTHENLAST
-				(Tacmach.internal_cut_no_check name newt)
-				(tclTHEN (Tactics.revert [name]) (Tactics.refine p))
-			| Some (t, ty) -> 
-			    Tactics.refine
-			      (mkApp (mkLambda (Name (id_of_string "newt"), newt,
-					       mkLambda (Name (id_of_string "lemma"), ty,
-							mkApp (p, [| mkRel 2 |]))),
-				     [| mkMeta goal_meta; t |])))
-	      in
-	      let evartac = 
-		let evd = Evd.evars_of undef in
-		  if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd)
-		  else tclIDTAC
-	      in tclTHENLIST [evartac; rewtac] gl
-	    with 
-	    | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
-	    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-		  tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints." 
-			      ++ fnl () ++ Himsg.explain_typeclass_error env e) gl)
-(* 	      | Not_found -> *)
-(* 		  tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl) *)
-      | None -> 
-	  let {l2r=l2r; c1=x; c2=y} = !hypinfo in
-	    raise (Pretype_errors.PretypeError 
-		      (pf_env gl, 
-		      Pretype_errors.NoOccurrenceFound ((if l2r then x else y), is_hyp)))
-	      (* tclFAIL 1 (str"setoid rewrite failed") gl *)
+    | Some (p, (_, _, oldt, newt)) -> 
+	(try 
+	  evars := Typeclasses.resolve_typeclasses env ~fail:true !evars;
+	  let p = Evarutil.nf_isevar !evars p in
+	  let newt = Evarutil.nf_isevar !evars newt in
+	  let undef = Evd.undefined_evars !evars in
+	  let abs = Option.map (fun (x, y) -> Evarutil.nf_isevar !evars x,
+	    Evarutil.nf_isevar !evars y) !hypinfo.abs in
+	  let rewtac = 
+	    match is_hyp with
+	    | Some id -> 
+		let term = 
+		  match abs with
+		  | None -> p
+		  | Some (t, ty) -> 
+		      mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
+		in
+		  cut_replacing id newt 
+		    (fun x -> Tactics.refine (mkApp (term, [| mkVar id |])))
+	    | None -> 
+		(match abs with
+		| None -> 
+		    let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+		      tclTHENLAST
+			(Tacmach.internal_cut_no_check name newt)
+			(tclTHEN (Tactics.revert [name]) (Tactics.refine p))
+		| Some (t, ty) -> 
+		    Tactics.refine
+		      (mkApp (mkLambda (Name (id_of_string "newt"), newt,
+				       mkLambda (Name (id_of_string "lemma"), ty,
+						mkApp (p, [| mkRel 2 |]))),
+			     [| mkMeta goal_meta; t |])))
+	  in
+	  let evartac = 
+	    let evd = Evd.evars_of undef in
+	      if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd)
+	      else tclIDTAC
+	  in tclTHENLIST [evartac; rewtac] gl
+	  with 
+	  | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+	  | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+	      tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints." 
+			  ++ fnl () ++ Himsg.explain_typeclass_error env e) gl)
+	  (* 	      | Not_found -> *)
+	  (* 		  tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl) *)
+    | None -> 
+	let {l2r=l2r; c1=x; c2=y} = !hypinfo in
+	  raise (Pretype_errors.PretypeError 
+		    (pf_env gl, 
+		    Pretype_errors.NoOccurrenceFound ((if l2r then x else y), is_hyp)))
+	    (* tclFAIL 1 (str"setoid rewrite failed") gl *)
 	  
+let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl =
+  try cl_rewrite_clause_aux ~flags hypinfo goal_meta occs clause gl
+  with DependentMorphism -> tclFAIL 0 (str " setoid rewrite failed: cannot handle dependent morphisms") gl
+
 let cl_rewrite_clause c left2right occs clause gl =
   init_setoid ();
   let meta = Evarutil.new_meta() in
@@ -1046,20 +1065,32 @@ VERNAC COMMAND EXTEND Typeclasses_Settings
 END
 
 TACTIC EXTEND typeclasses_eauto
-| [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ fun gl ->
-    let env = pf_env gl in
-    let sigma = project gl in
-      if Evd.dom sigma = [] then Refiner.tclIDTAC gl
-      else
-	let evd = Evd.create_evar_defs sigma in
-	let mode = match s with Some t -> t | None -> true in
-	let depth = match depth with Some i -> i | None -> default_eauto_depth in
-	  match resolve_typeclass_evars d (mode, depth) env evd false with
-	    | Some evd' -> Refiner.tclEVARS (Evd.evars_of evd') gl
-	    | None -> tclIDTAC gl
-  ]
+| [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ 
+    let mode = match s with Some t -> t | None -> true in
+    let depth = match depth with Some i -> i | None -> default_eauto_depth in
+      fun gl -> 
+	let gls = {it = [sig_it gl]; sigma = project gl} in
+	let vals v = List.hd v in
+	  typeclasses_eauto d (mode, depth) [] (gls, vals) ]
 END
 
+
+(*     fun gl -> *)
+(*     let env = pf_env gl in *)
+(*     let sigma = project gl in *)
+(*     let proj = sig_it gl in *)
+(*     let evd = Evd.create_evar_defs (Evd.add Evd.empty 1 proj) in *)
+(*     let mode = match s with Some t -> t | None -> true in *)
+(*     let depth = match depth with Some i -> i | None -> default_eauto_depth in *)
+(*       match resolve_typeclass_evars d (mode, depth) env evd false with *)
+(*       | Some evd' ->  *)
+(* 	  let goal = Evd.find (Evd.evars_of evd') 1 in *)
+(* 	    (match goal.evar_body with *)
+(* 	    | Evar_empty -> tclIDTAC gl *)
+(* 	    | Evar_defined b -> refine b gl) *)
+(*       | None -> tclIDTAC gl *)
+(*   ] *)
+
 let _ = 
   Classes.refine_ref := Refine.refine
 
@@ -1316,7 +1347,8 @@ let default_morphism sign m =
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let t = Typing.type_of env Evd.empty m in
   let _, sign, evars =
-    build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
+    try build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
+    with DependentMorphism -> error "Cannot infer the signature of dependent morphisms"
   in
   let morph =
     mkApp (Lazy.force morphism_type, [| t; sign; m |])
@@ -1339,7 +1371,9 @@ let add_setoid binders a aeq t n =
 let add_morphism_infer m n =
   init_setoid ();
   let instance_id = add_suffix n "_Morphism" in
-  let instance = build_morphism_signature m in
+  let instance = try build_morphism_signature m 
+    with DependentMorphism -> error "Cannot infer the signature of dependent morphisms"
+  in
     if Lib.is_modtype () then 
       let cst = Declare.declare_internal_constant instance_id
 	(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v
index 2d0991cb1..22c3df824 100644
--- a/test-suite/bugs/closed/shouldsucceed/1604.v
+++ b/test-suite/bugs/closed/shouldsucceed/1604.v
@@ -3,5 +3,5 @@ Require Import Setoid.
 Parameter F : nat -> nat.
 Axiom F_id : forall n : nat, n = F n.
 Goal forall n : nat, F n = n.
-intro n. setoid_rewrite F_id at 2. reflexivity.
+intro n. setoid_rewrite F_id at 3. reflexivity.
 Qed.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 6885d0b29..0d464b84e 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -28,6 +28,21 @@ Unset Strict Implicit.
    We now turn to the definition of [Morphism] and declare standard instances. 
    These will be used by the [setoid_rewrite] tactic later. *)
 
+(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
+   for usual morphisms. *)
+
+Class Morphism A (R : relation A) (m : A) : Prop :=
+  respect : R m m.
+
+(** We make the type implicit, it can be infered from the relations. *)
+
+Implicit Arguments Morphism [A].
+
+(** We allow to unfold the [relation] definition while doing morphism search. *)
+
+Typeclasses unfold relation.
+
 (** Respectful morphisms. *)
 
 (** The fully dependent version, not used yet. *)
@@ -49,6 +64,7 @@ Definition respectful (A B : Type)
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
 Delimit Scope signature_scope with signature.
+Arguments Scope Morphism [type_scope signature_scope].
 
 Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
   (right associativity, at level 55) : signature_scope.
@@ -63,22 +79,18 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
-(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
-   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
-   for usual morphisms. *)
-
-Class Morphism A (R : relation A) (m : A) : Prop :=
-  respect : R m m.
-
-Arguments Scope Morphism [type_scope signature_scope].
-
-(** We make the type implicit, it can be infered from the relations. *)
-
-Implicit Arguments Morphism [A].
+(** We can build a PER on the Coq function space if we have PERs on the domain and
+   codomain. *)
 
-(** We allow to unfold the [relation] definition while doing morphism search. *)
+Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
+  PER (A -> B) (R ==> R').
 
-Typeclasses unfold relation.
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0). 
+    transitivity y0... symmetry...
+    transitivity (y x0)...
+  Qed.
 
 (** Subrelations induce a morphism on the identity, not used for morphism search yet. *)
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 17a645c8f..044195f19 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -162,26 +162,19 @@ Class PER (carrier : Type) (pequiv : relation carrier) : Prop :=
   PER_Symmetric :> Symmetric pequiv ;
   PER_Transitive :> Transitive pequiv.
 
-(** We can build a PER on the Coq function space if we have PERs on the domain and
-   codomain. *)
-
-Program Instance arrow_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B)
-  (fun f g => forall (x y : A), R x y -> R' (f x) (g y)).
-
-  Next Obligation.
-  Proof with auto.
-    assert(R x0 x0). 
-    transitivity y0... symmetry...
-    transitivity (y x0)...
-  Qed.
-
-(** The [Equivalence] typeclass. *)
+(** Equivalence relations. *)
 
 Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
   Equivalence_Reflexive :> Reflexive equiv ;
   Equivalence_Symmetric :> Symmetric equiv ;
   Equivalence_Transitive :> Transitive equiv.
 
+(** An Equivalence is a PER plus reflexivity. *)
+
+Instance Equivalence_PER [ Equivalence A R ] : PER A R :=
+  PER_Symmetric := Equivalence_Symmetric ;
+  PER_Transitive := Equivalence_Transitive.
+
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
 Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index a9ad92f4c..d5d8702bc 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -170,11 +170,14 @@ let firstchar =
   ['A'-'Z' 'a'-'z' '_' 
   (* iso 8859-1 accents *) 
   '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  '\194' '\185' |
   (* utf-8 latin 1 supplement *) 
   '\195' ['\128'-'\191'] |
   (* utf-8 letterlike symbols *) 
   '\206' ['\177'-'\183'] |
-  '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+  '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+    | '\129' [ '\176'-'\187' ] (* superscripts *)
+    | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
 let identchar = 
   firstchar | ['\'' '0'-'9' '@' ]
 let id = firstchar identchar*