diff options
| author | herbelin | 2001-02-14 15:41:55 +0000 |
|---|---|---|
| committer | herbelin | 2001-02-14 15:41:55 +0000 |
| commit | e7d592ada2d681876d2bcf0a45d4267b3746064f (patch) | |
| tree | e0b7eb1e67b1871b7cb356c33f66182f6dde86c3 /toplevel/class.ml | |
| parent | 045c85f66a65c6aaedeed578d352c6de27d5e6a4 (diff) | |
Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index e0ae40af60..4d8e5ba2cd 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -8,6 +8,7 @@ open Term open Inductive open Declarations open Environ +open Inductive open Lib open Classops open Declare @@ -260,18 +261,16 @@ let build_id_coercion idf_opt source = | Some c -> c | None -> error_not_transparent source in let lams,t = Sign.decompose_lam_assum c in - let llams = List.length lams in - let lams = List.rev lams in let val_f = it_mkLambda_or_LetIn (mkLambda (Name (id_of_string "x"), - applistc vs (rel_list 0 llams), + applistc vs (extended_rel_list 0 lams), mkRel 1)) lams in let typ_f = it_mkProd_wo_LetIn - (mkProd (Anonymous, applistc vs (rel_list 0 llams), lift 1 t)) + (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t)) lams in (* juste pour verification *) @@ -387,7 +386,7 @@ let count_extra_abstractions hyps ids_to_discard = List.fold_left (fun (hyps,n as sofar) id -> match hyps with - | (hyp,None,_)::rest when id = hyp ->(rest, n+1) + | (hyp,None,_)::rest when id = basename hyp ->(rest, n+1) | _ -> sofar) (hyps,0) ids_to_discard in n |