From ead31bf3e2fe220d02dec59dce66471cc2c66fce Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Aug 2003 10:25:04 +0000
Subject: Nouvelle mouture du traducteur v7->v8 Option -v8 à coqtop lance
 coqtopnew Le terminateur reste "." en v8 Ajout construction primitive
 CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les
 Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la
 traduction Ajout option -no-strict pour traduire les "Set Implicits" en
 implicites stricts + Bugs ou améliorations diverses Raffinement affichage
 projections de Record/Structure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/psyntax.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/correctness/psyntax.ml4')

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 0e6b3b7d2f..2e3fcac411 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -107,7 +107,7 @@ open Coqast
 let mk_id loc id = mkRefC (Ident (loc, id))
 let mk_ref loc s = mk_id loc (id_of_string s)
 let mk_appl loc1 loc2 f args =
-  CApp (join_loc loc1 loc2, (false,mk_ref loc1 f), List.map (fun a -> a,None) args)
+  CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args)
 
 let conj_assert {a_name=n;a_value=a} {a_value=b} = 
   let loc1 = constr_loc a in
@@ -166,7 +166,7 @@ let rec coqast_of_program loc = function
 		   (function Term t -> (coqast_of_program t.loc t.desc,None)
 		      | _ -> invalid_arg "coqast_of_program") l
       in
-      CApp (dummy_loc, (false,f), args)
+      CApp (dummy_loc, (None,f), args)
   | Expression c -> bdize c
   | _ -> invalid_arg "coqast_of_program"
 
-- 
cgit v1.2.3