diff options
| author | herbelin | 2005-12-17 21:07:17 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-17 21:07:17 +0000 |
| commit | cea2061080d540c0507192eca1887ea4b502680d (patch) | |
| tree | 4eee8420ee1cead95242a0dc6a5ea47f6b5fc39f /toplevel/command.ml | |
| parent | d7e634b61c0f6db8f2593fbdd5de8f8418beb84a (diff) | |
Orthographe de 'instantiate'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 0c916f7038..f64bae5a19 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -221,7 +221,7 @@ let declare_one_elimination ind = let sigma = Evd.empty in let elim_scheme = Indrec.build_indrec env sigma ind in let npars = mib.mind_nparams_rec in - let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in + let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in let kelim = mip.mind_kelim in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the @@ -232,7 +232,7 @@ let declare_one_elimination ind = let c = mkConst cte and t = constant_type (Global.env()) cte in List.iter (fun (sort,suff) -> let (t',c') = - Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort) + Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort) npars c t in let _ = declare (mindstr^suff) c' (Some t') in ()) non_type_eliminations |