diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-22 18:09:11 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-22 18:09:11 +0000 |
| commit | 66ee7ba58080fa8fcfdb4bb76b89cc0b70a8a4ac (patch) | |
| tree | e97e3bd30fa49fc5da4dfe207ff73e841ee083b1 /contrib | |
| parent | fe027346f901f26d79ce243a06c08a8c9f661e81 (diff) | |
traducteur: affiche les commentaires a l'interieur des commandes
extraction: pb avec les variables de section definies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/extraction.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index a4c2cc46e..df1069c18 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -352,10 +352,11 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let n = nb_default_params env mip0.mind_nf_arity in let projs = try List.map out_some projs with _ -> raise (I Standard) in let is_true_proj kn = - match kind_of_term (snd (decompose_lam (constant_value env kn))) with - | Rel _ -> false - | Case _ -> true - | _ -> assert false + let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in + match kind_of_term body with + | Rel _ -> false + | Case _ -> true + | _ -> assert false in let projs = List.filter is_true_proj projs in let rec check = function |