diff options
| author | sacerdot | 2004-10-05 18:47:26 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-05 18:47:26 +0000 |
| commit | f0c3fac1876a8be5e3b55201b1a800f9af377374 (patch) | |
| tree | 6672eb55006361d0199d1342815cbf9b56ae1f0c /tactics/setoid_replace.ml | |
| parent | 691bb5a14ed0be69b70db0dfa0d4dcae280d2cd4 (diff) | |
* code simplification
* error message improved
* bug fixed: it was not checked whether the carrier of a relation of class
Leibniz matched the expected type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6180 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index ac0858a9de..be1105e17e 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -688,7 +688,7 @@ let apply_to_relation subst rel = let unify_relation_carrier_with_type env rel t = let raise_error () = errorlabstrm "New Morphism" - (str "One morphism argument has type " ++ prterm t ++ + (str "One morphism argument or its output has type " ++ prterm t ++ str " but the signature requires an argument of type (" ++ prterm rel.rel_a ++ str " ? ... ?)") in let args = @@ -711,7 +711,14 @@ let unify_relation_carrier_with_type env rel t = let unify_relation_class_carrier_with_type env rel t = match rel with - Leibniz _ -> rel + Leibniz t' -> + if is_conv env Evd.empty t t' then + rel + else + errorlabstrm "New Morphism" + (str "One morphism argument or its output has type " ++ prterm t ++ + str " but the signature requires an argument of type " ++ + prterm t') | Relation rel -> Relation (unify_relation_carrier_with_type env rel t) (* first order matching with a bit of conversion *) @@ -791,15 +798,9 @@ let new_morphism m signature id hook = | Some (args,output') -> let find_relation_class t real_t = try - match find_relation_class t with -(*CSC: mi sa che anche l'inference del tipo per Leibniz e' bacata... - cosa succede se ho un morfismo (incl A) --> (@eq A) --> impl - Leibniz dovrebbe essere sempre quantificata, ma nel modo giusto! ?*) - (Leibniz _) as rel -> rel,rel - | Relation rel -> - Relation rel, - Relation - (unify_relation_carrier_with_type (Global.env ()) rel real_t) + let rel = find_relation_class t in + rel, + unify_relation_class_carrier_with_type (Global.env ()) rel real_t with Not_found -> errorlabstrm "Add Morphism" (str "Not a valid signature: " ++ prterm t ++ |