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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_xml.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 99cfa70838..621aab8a03 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -146,8 +146,8 @@ let compute_branches_lengths ind = let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in mip.Declarations.mind_consnrealdecls -let compute_inductive_nargs ind = - Inductiveops.inductive_nargs ind +let compute_inductive_ndecls ind = + snd (Inductiveops.inductive_ndecls ind) (* Interpreting constr as a glob_constr *) @@ -188,7 +188,7 @@ let rec interp_xml_constr = function let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl in let mat = simple_cases_matrix_of_branches ind brs in - let nparams,n = compute_inductive_nargs ind in + let n = compute_inductive_ndecls ind in let nal,rtn = return_type_of_predicate ind n p in GCases (loc,RegularStyle,rtn,[tm,nal],mat) | XmlTag (loc,"MUTIND",al,[]) -> |