diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-24 17:56:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-24 17:56:05 +0000 |
| commit | 33c03c270a2380c8462914b02c3355d4a5cea273 (patch) | |
| tree | ba4523cbe3a09608a623b71ef63183aacdec8aaa | |
| parent | 5a09134ebee8d92d9ed05d04d2808a30a2d83900 (diff) | |
Simplifications concommitantes à la correction du bug #855
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6126 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/equality.mli | 3 | ||||
| -rw-r--r-- | tactics/inv.ml | 7 |
2 files changed, 4 insertions, 6 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 6b405b247..672c4014a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -55,8 +55,7 @@ val dEq : quantified_hypothesis option -> tactic val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic val make_iterated_tuple : - env -> evar_map -> (constr * constr) -> (constr * constr) - -> constr * constr * constr + env -> evar_map -> constr -> (constr * types) -> constr * constr * constr val substHypInConcl : bool -> identifier -> tactic val substConcl : bool -> constr -> tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index 22f7009e9..b09703369 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -88,8 +88,7 @@ let var_occurs_in_pf gl id = type inversion_status = Dep of constr option | NoDep let compute_eqn env sigma n i ai = - (ai,get_type_of env sigma ai), - (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) + (ai, (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))) let make_inv_predicate env sigma indf realargs id status concl = let nrealargs = List.length realargs in @@ -128,12 +127,12 @@ let make_inv_predicate env sigma indf realargs id status concl = In any case, we carry along the rest of pairs *) let rec build_concl eqns n = function | [] -> (prod_it concl eqns,n) - | ((ai,ati),(xi,ti))::restlist -> + | (ai,(xi,ti))::restlist -> let (lhs,eqnty,rhs) = if closed0 ti then (xi,ti,ai) else - make_iterated_tuple env' sigma (ai,ati) (xi,ti) + make_iterated_tuple env' sigma ai (xi,ti) in let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in let sort = get_sort_of env sigma concl in |