diff options
| author | Hugo Herbelin | 2014-08-01 14:27:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-01 14:27:23 +0200 |
| commit | 128a297614d1e0fb32e2bbd465d181c5d5b1562c (patch) | |
| tree | 1677d5a840c68549cf6530caf2929476a85ad68a /interp/constrextern.ml | |
| parent | d89eaa87029b05ab79002632e9c375fd877c2941 (diff) | |
A tentative uniform naming policy in module Inductiveops.
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5ce7f8f91d..9c2f8bcd3f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -165,7 +165,7 @@ let in_debugger = ref false let add_patt_for_params ind l = if !in_debugger then l else - Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -275,7 +275,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = not explicit application. *) match pat with | PatCstr(loc,cstrsp,args,na) - when !in_debugger||Inductiveops.mis_constructor_has_local_defs cstrsp -> + when !in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) |